System F
多相λ計算 (polymorhic lambda calculus)。二階λ計算 (second-order lambda calculus)$ \lambda 2
項
項$ tが型變數$ \alphaを自由變數として含む事を明示する場合は$ t(\alpha)と書く
$ \alphaが型變數で$ tが項ならば$ \Lambda\alpha.tも項である (Λ抽象)
$ tが項で$ Aが型ならば$ t~Aも項である
型
$ \alphaが型變數で$ Aが型ならば$ \forall\alpha.Aも型である (全稱型。多相型) 型$ T_1 が型變數$ \alpha を自由變數として含む$ T_1(\alpha) として、型變數$ \alpha に型$ T_2 を代入したもの$ T_1[T_2/\alpha] も型である
推論規則
Λ抽象$ \frac{\Gamma,\alpha~{\rm type}\vdash t:A}{\Gamma\vdash\Lambda\alpha.t:\forall\alpha.A}({\rm TABS})
.
$ \frac{\Gamma\vdash t:\forall\alpha.A}{\Gamma\vdash t~B:A[B/\alpha]}({\rm TAPP})
System Fω
System F<: